Termination Proof Script
Consider the TRS R consisting of the rewrite rule
1:
ap
(
ap
(
ff
,x),x)
→
ap
(
ap
(x,
ap
(
ff
,x)),
ap
(
ap
(
cons
,x),
nil
))
There are 4 dependency pairs:
2:
AP
(
ap
(
ff
,x),x)
→
AP
(
ap
(x,
ap
(
ff
,x)),
ap
(
ap
(
cons
,x),
nil
))
3:
AP
(
ap
(
ff
,x),x)
→
AP
(x,
ap
(
ff
,x))
4:
AP
(
ap
(
ff
,x),x)
→
AP
(
ap
(
cons
,x),
nil
)
5:
AP
(
ap
(
ff
,x),x)
→
AP
(
cons
,x)
The approximated dependency graph contains one SCC: {2,4}.
Consider the SCC {2,4}.
The constraints could not be solved.
Tyrolean Termination Tool
(0.02 seconds) --- May 3, 2006